module mult (
	A, B, P, rst, clk, vld, move, part, step, tick
);

parameter WIDTH = 4;

input rst, clk;
input [WIDTH-1: 0] A, B;
output reg [2*WIDTH-1: 0] P;
output reg vld;

output reg [WIDTH-1: 0] part, part_comp;
output reg [2*WIDTH-1: 0] move;
output reg [$clog2(WIDTH+1)-1: 0] step;
output reg tick;

reg c;
reg q;

// MBFA is assumed to have independent clock, or simply a combinational
// logic. part will be updated as long as any of inputs changes.
multi_bit_full_adder #(.WIDTH(WIDTH)) mbfa (.A(move[2*WIDTH-1: WIDTH]), .B(B), .S(part));
multi_bit_full_adder #(.WIDTH(WIDTH)) mbfa_comp (.A(move[2*WIDTH-1: WIDTH]), .B(~B+1'b1), .S(part_comp));

// reset all intermediate stuff 
always @ (posedge rst) begin
	if (rst) begin
		move <= {{WIDTH{1'b0}}, A};
		step <= 0;
		tick <= 0;
		q <= 0;
		P <= 0;
		vld <= 0;
	end
end

// build a shifting signal tick. When tick is high, shift partial product,
// when tick is low, add up with multiplicand on that bit.

always @ (posedge clk) begin
	if (step < WIDTH) begin
		if (tick) begin
			//{move, q} <= {0, move};
			{move, q} <= {move[2*WIDTH-1], move};
			step <= step + 1;
		end else if (move[0] && !q) begin
			move[2*WIDTH-1: WIDTH] <= part_comp; 
		end else if (!move[0] && q) begin
			move[2*WIDTH-1: WIDTH] <= part; 
		end

		tick <= ~tick;
		vld <= 0;

	end else begin
		P <= move[2*WIDTH-1: 0];
		vld <= 1;
	end
end

endmodule

module mult_verification;

parameter WIDTH = 4;

input rst, clk;
input [WIDTH-1: 0] A, B;
input reg [2*WIDTH-1: 0] P;
input reg vld;
input reg [WIDTH-1: 0] part, part_comp;
input reg [2*WIDTH-1: 0] move;
input reg [$clog2(WIDTH+1)-1: 0] step;
input reg tick;

property tick_after_reset;
	@(posedge clk) rst |-> ##3 tick;
endproperty

assert property (tick_after_reset);

endmodule
